abstract class $ARR{ETP} < $RO_ARR{ETP} |
---|
**** | The indices are integers and lie in [0, size-1] Similar to a MAP from ints to elements, but more restrictive conditions The features are repeated here so as to restate the preconditions Inherits: copy, size, capacity, elt! and has size: INT; elt!: ETP; has(e: ETP): BOOL; |
$RO_ARR{_} | $CONTAINER{_} | $ELT{_} | $ELT |
aget(i: INT): ETP; |
---|
**** | pre has_ind(i) |
aset(ind: INT,e: ETP); |
---|
**** | pre has_ind(i) |
copy: $ARR{ETP}; |
---|
**** | Redefined to narrow the return type |
has_ind(i: INT): BOOL; |
---|
**** | return 0<=i<size This method could actually be implemented at this level |
ind!: INT; |
---|
**** | post 0<=result<size Returns all the indices, which are the integers between 0 and size - 1 |